1. $P$ : $\mathbb{P}$ \\[0ex]2. $x$ : $P$ \\[0ex]3. $P$ \\[0ex]$\vdash$ $\uparrow$[inl $x$ ]$_{b}$